Битва зависимых элиминаторов Bool

TL;DR: По мотивам Issue: https://github.com/groupoid/exe/issues/7

Как вы знаете ленивость является фундаментальным свойтсвом всех (!) без
исключения языков программирования, которые хотят или стремятся к тому, чтобы
быть внутренними языками декартово замкнутой категории, или как говорят
механизаторы — лямбда исчислением.

Почему так? Чтобы закодировать условный оператор if без которого не обходится
ни один язык программирования, в чистом лямбда ичсислении нам не обойтись без
ленивости. Напишем энергичный оператор if для Bool типа (который как мы знаем
совпадает со всеми кодировками, Church, Scott, Parigot, CPS и другими
возможными, так как у его все конструкторы без параматеров, а кодировки обычно
с параметрами работают).

Вот наш тип Bool записаный на языке OM:

$ cat @
∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool

$ cat True
λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → True

$ cat False
λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → False

И вот жадный элиминатор eif:

$ cat eif
  λ (A : *)
→ λ (X : #Bool/@)
→ λ (Y : A)
→ λ (Z : A)
→ X A Y Z

Если мы скомпилируем его (т.е. сотрем информацию о типах), заэкстрактим в
эрланг код, вытащим эрланг код и вставим в одну ветку оператор printf
(io:format в эрланге), то при вызове этой функции eif у нас выполнятся обеи эти
ветки. Вот пример использования оператора eif:

$ cat eiff
    \ (X: #Bool/@)
->  \ (Y: #Nat/@)
-> #Bool/eif #Nat/@ X
   (#Nat/[+] Y (#Nat/Succ (#Nat/Succ (#Nat/Succ (#Nat/Succ (#Nat/Succ
#Nat/Zero))))))
   (Y)

Тут мы вызываем условие eiff x y = if x then y + 5 else y. Так вот если
вытащить ненормализированый эрланг терм и вставить в ветку с Succ printf, то
при вызове eiff c True и False будет печататься этот printf:

> ch:unnat(ch:ap(eiff:eiff(),['Bool':'False'(),'Nat':'Zero'()])).
EIFF
0
123> ch:unnat(ch:ap(eiff:eiff(),['Bool':'True'(),'Nat':'Zero'()])).
EIFF
5

Выход к этому лежит через тип Lazy:

$ cat @
\ (a: *) -> \ (x: a) -> \ (y: #Unit/@) -> x

$ cat delay
\ (a: *) -> \ (delay: #Unit/@ -> a) -> #Lazy/@ a

$ cat force
\ (a: *) -> \ (force: #Unit/@ -> a) -> a

Мы переписываем наш eif на ленивый if:

$ cat if
  λ (A : *)
→ λ (X : #Bool/@)
→ λ (Y : #Unit/@ → A)
→ λ (Z : #Unit/@ → A)
→ X (#Unit/@ → A) Y Z #Unit/Make

и пример:

$ cat iff
    \ (X: #Bool/@)
->  \ (Y: #List/@ #Nat/@)
-> #Bool/if #Nat/@ X
   (\ (l: #Unit/@) -> #List/length #Nat/@
   (#List/Cons #Nat/@ #Nat/Zero
   (#List/Cons #Nat/@ #Nat/Zero
   (#List/Cons #Nat/@ #Nat/Zero
   (#List/Cons #Nat/@ #Nat/Zero
   (#List/Cons #Nat/@ #Nat/Zero
   (#List/Cons #Nat/@ #Nat/Zero
   (#List/Cons #Nat/@ (#Nat/Succ #Nat/Zero) Y))))))))
   (\ (p: #Unit/@) -> #List/length #Nat/@ Y)

который соотвествует iff x y = if x then list.length [0,0,0,0,0,0,1|y] else
lists.length y.

Скомпилируем это в эрланг:

> om:extract("priv/normal/Bool").
ok

Теперь вытащим из него код:

> l('Bool').
{module,'Bool'}
> {ok,{_,[{abstract_code,{_,AC9}}]}} =
beam_lib:chunks("ebin/Bool.beam",[abstract_code]).
ok
> io:fwrite("~s~n", [erl_prettypr:format(erl_syntax:form_list(AC9))]).

Находит там функцию iff и сохраняем в файл iff.erl. Вставляем в ветке с Cons
io:format("IFF!~n"), и проверяем:

> ch:unnat(ch:ap(iff:iff(),['Bool':'True'(),'List':'Nil'()])).
IFF!
7
11> ch:unnat(ch:ap(iff:iff(),['Bool':'False'(),'List':'Nil'()])).
0

Напоминаю что все происходило с выключенной нормализацией в om_extract:

extract(F,om:fst(om:erase(om:snd(om:parse(om:read(X++"/"++F))))),1)

если включить нормализацию:

extract(F,om:fst(om:erase(om:normal(om:snd(om:parse(om:read(X++"/"++F)))))),1)

то даже (!) c Eager IF все работает как нада (т.е. заходит в одну ветку),
опускаю подробности публикую Матрицу:

Norm Lazy Cnt
==== ==== ====

+    +    1
+    -    1
-    +    1
-    -    2       (unsatisfied case for runtime, two branch)

Теперь смотрим как сделано в других языках:

https://github.com/idris-lang/Idris-dev/blob/master/src/IRTS/Compiler.hs#L289-L303
https://github.com/idris-lang/Idris-dev/blob/master/src/Idris/Elab/Type.hs#L232-L248
https://github.com/idris-lang/Idris-dev/blob/master/src/Idris/Core/Unify.hs#L714-L717
https://github.com/idris-lang/Idris-dev/blob/master/src/Idris/Core/Evaluate.hs#L123-L140

https://www.cs.ox.ac.uk/projects/utgp/school/idris-tutorial.pdf

data Lazy : Type -> Type where Delay : (val : a) -> Lazy a
   Force : Lazy a -> a


A value of type Lazy a is unevaluated until it is forced by Force. The Idris
type checker knows about the Lazy type, and inserts conversions where necessary
between Lazy a and a, and vice versa. We can therefore write boolCase as
follows, without any
explicit use of Force or Delay:

   boolCase : Bool -> Lazy a -> Lazy a -> a
   boolCase True  t e = t
   boolCase False t e = e

Т.е. сделано точно также как в Om, или другими словами через добавление обычной
лямбды () -> A вместо A. Просто зашито в дешугаринге, чтобы программист сам
force не писал.

Вот такая петрушка. NPONECCOP патается копать глубже, но глубже у меня не
получается, не вижу статей которые опровергали бы эти простые размышления и
находили более глубокие подводные камни.